@jhoenicke I found that without this change there's no way to use a logical formula containing a constant string, not even the simplest (= x "hello").

I think this is unsound without any String reasoning. E.g., with this change, SMTInterpol will also say that (and (= x "hello") (= x "good bye")) is satisfiable.

I'm happy to devote some time to have this working; is there any place I could look at to bring strings to SMTInterpol?

Writing a string solver can be quite an involved task. The whole theory is undecidable, so the first step would be to pick a decidable fragment and an algorithm for this fragment. Here is a survey on techniques of string solving: https://arxiv.org/pdf/2002.02376.pdf

If you want to work on a solver, I can help you to integrate it in SMTInterpol.